[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

MASTERARBEIT

Titel der Masterarbeit

On Hilbert’s Tenth Problem over

Rings of Algebraic Integers

verfasst von

Tim Benedikt Herbstrith BSc

angestrebter akademischer Grad

Master of Science (MSc)

Wien, 2019

Studienkennzahl lt. Studienblatt: A 033 821

Studienrichtung lt. Studienblatt: Mathematik

Betreut von: ao. Univ.-Prof. Mag. Dr. Ch. Baxa

[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

                   

          

                  

                

             

https://github.com/tim6her/h10-over-rings-of-integers

Some Rights

Reserved

[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

Contents

1 Prerequisites and central notions 1

                           

                      

                      

                               

                                

                        

                     

                              

                        

   



                                

                               

                             

2 Hilbert’s tenth problem 57

                             

                           

                              

                                 

                                   

               

                              

                          

A Collected Haskell implementations 103

                                

                                       

B Summaries 111

                                   

                                        



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

1 Prerequisites and central notions

                

                  

               

             

           

               

                

                

                

              

               

               



           









1.1 Prerequisites from computability theory

            

          

            



              

            

                  

             

           

               

            

                

          

                   

              

                

                 

         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

1 3

≅

↕

𝑥 = 101

≠

𝑦 = 011

↕

       

1.1.1 Turing machines, problems, and decidability

       01   01



     

               01   

  0  1   

               

         

           



                

              

 





         



              

               

         

 







 







 



 







              

               



1 

           

     

101  011       



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

         

                 

               

                 

                    

          §             

          _       

  

       §_01      

            

start



halt

  



    



     

 §     §

  §   

  

halt

 





halt

  

                

                 

               

                 

    

       §          

              

      

halt

          

 

                   

    0            

 0     

overow

   



overow

0

return

1

              

return

  

 1                  

    

overow

0          

               

 

               





                 

  



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

0 0 0 1

. . .

overflow

    

     

halt

         



start

  §       _     

         

§__

              

                 

 

§001_0__

                



01



 

      











        









§  





 

_ 

   











       

 















  











       

 

 









 



 

 



  

              

                   

 

start

              



halt

                

  

           

delta



state



state’







  

delta "state" b = ("state'", b', m)

             

               

     



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

          

-- start by entering the "overflow" state ...

add1 "start" '§' = ("overflow", '§', 1 )

-- ... and stay in this state, as long as you read only '1'-s

add1 "overflow" '1' = ("overflow", '0', 1 )

-- if you read the first '0' or an empty cell replace it by '1'

-- and enter the "return" state to move the head to the first cell

add1 "overflow" '0' = ("return", '1', -1)

add1 "overflow" '_' = ("return", '1', -1)

-- we finish if we read '§' again or ...

add1 "return" '§' = ("halt", '§', 0 )

-- ... continue to move to the left and don't change the cell

-- content. Here `b` matches '0' or '1'

add1 "return" b = ("return", b , -1)

add1 _state _char = ("error", '_', 0 )

delta "state" 1 = ("state'", b', m )

delta "state" b = ("state''", b'', m')

   







state’





  

state

1



state”









  

state

1



              

              



            

      

add1



start



halt



overow



return



error



add1



              

                   

               

error



    

add1

 1101           

         1101     













     

                

        

     1     0

     01



         

          

 https://www.haskell.org/onlinereport/haskell2010



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

1 1 0 1

. . .

start

 

start

§

overow

§

1 1 0 1

. . .

overflow

 

overow

1

overow

0

0 1 0 1

. . .

overflow

 

overow

1

overow

0

0 0 0 1

. . .

overflow

 

overow

0

return

1

0 0 1 1

. . .

return

 

return

0

return

0

0 0 1 1

. . .

return

 

return

0

return

0

0 0 1 1

. . .

return

 

return

§

halt

§

0 0 1 1

. . .

halt

 

halt

§

halt

§

      

add1

 1101



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

   01



       

  

              

      

                 

            



                 

           







start



halt



reject

























 





            



start





      











1













1  



reject

_ 











0













0  



reject

_ 











_





_  











reject

_  











                









     

























                   

               

              

         

       _            

    

                 

        

          







   

 

          1    

reject

   

     0  



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                 

        

 

reject

    

                

    

                 



   











 











     









 







  







       

  









    





















 

 



 





  

start



halt

  



  



     

      





start

§

halt

§  



    

     















              









 









   















start



halt



 















start



halt



   





start



halt























compose



             

 

















  











start





compose

  



 





halt











  











halt









start

  

compose

 









 







         



 

       





        

   

 11



-times

  



     





























1  

0



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

          

-- start by entering the "check" state and ...

tally "start" '§' = ("check", '§', 1 )

-- ... stay in this state while reading only '1'-s

tally "check" '1' = ("check", '1', 1 )

-- on reading '_' accept the input and clear the tape ...

tally "check" '_' = ("accept", '_', -1)

tally "accept" '1' = ("accept", '_', -1)

-- ...except for cell c(1), where you write a '1'

tally "accept" '§' = ("accept", '§', 1 )

tally "accept" '_' = ("halt", '1', -1)

-- however, if you read a '0' first, reject the input

-- by moving to the end of the input string ...

tally "check" '0' = ("rejectMR", '0', 1 )

tally "rejectMR" '_' = ("reject", '_', -1)

tally "rejectMR" b = ("rejectMR", b, 1 ) -- `b` matches '0' or '1'

-- ... and clear the tape except for cell c(1) where you

-- write a '0'

tally "reject" '§' = ("reject", '§', 1 )

tally "reject" '_' = ("halt", '0', -1)

tally "reject" b = ("reject", '_', -1) -- `b` matches '0' or '1'

tally _state _char = ("error", '_', 0 )

          

























  



            01



   





     



01





     

                   

        



01







                   

            1      

  



tally



start



halt



check



reject



rejectMR



error



            

          1          



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  



       



       

   



          

          



   



0

    

              

    



          

                 



 0

               

              

               





              

 























     















     

   







 



 





             

 





 11



-times

0 11



-times



                

    0      1      





    0     



         

    1       

        













































































01 













                  

               

 



              01

                 

               



    

        

                    

 §                   

                 

                     

                 

         

             



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

. . .

n−2

n−1

. . .

find non-empty

 The machine nds the rst non-empty cell.

. . .

n−2

n−1

. . .

shift left b

 The machine shifts the content of each cell one cell to the left …

. . .

n−1

. . .

shift left b

 … until it reaches the end of tape symbol §.

. . .

n−1

. . .

find __

 The machine nds two consecutive blank cells and starts over.

                

      



























      







    



     

             













                









           

  





  



            































     

               

              

  



      



   

  













 







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

           



   

  0   



  

   



      



 

  

    



             

             

                

                

     

              

      











   

§ 



__ 



__



               

           











   

                 

         

§ 



_







_







_





     



         

            



    

             

         

              

            

          

  

        

        

      



 

  

              

   1           1 

    

    



      1   1  

            



   

   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                

               

          

     







   

§















_

                 

                 

                 

 

§







_

                

 

                  

               

               

           







 







  

   



 

         

            



    

                

             

                   

               



  









 

           

   1           1   

   

              

         

           

                   

               

 

              





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            1

-- start by entering the "check" state

check1 "start" '§' = ("check", '§', 1 )

-- if you read a 1, check that the next cell is blank, and accept

check1 "check" '1' = ("check_blank", '1', 1 )

check1 "check_blank" '_' = ("accept", '_', -1)

-- if either of these conditions is not the case, reject

check1 "check" b = ("reject", b, 1 )

check1 "check_blank" b = ("reject", b, 1 )

-- accepting and rejecting actions

check1 "accept" 1 = ("halt", 1, -1)

check1 "reject" b = ("error", b, 1 )

check1 _state _char = ("error", '_', 0 )

              

         10  01  

            

              



             

            1

                

          1      

       



     















10100



0



0



0



0



0





             

          1      0    

         

      



       

       





         











    

     



     





     











            

               1      

           



  



 





       0            

                

   



             

             1       

       

             

     



        



    



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

           



   

            











   

       1  0         



 

halt

 





1.1.2 Church-Turing thesis and the halting problem

               

           

            

   

             

  

               

      

                

                 

                  

             

             

         

  

                  

                   

               

              

            

            

                

                 

             

             

      

               

    





1    

0      

             

         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                       

 

       



     

      1     





        

 



   

                

          





  



             

         

               

                 



   

               

      

  

   

         



   

    

  





                 

        



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  







            

                

              

       

  

    



    







   



 

   

  



    





 





   





 



    



          

           

 



   



            

         



  

  



   

        



       

 



      



 



     

               

          

        



   



    



 

                 

         



      



 

1.2 Prerequisites from model theory

           

             

                  

        

1.2.1 Formulae and models

              

              

             

                

               

              

      







     

                  

           

      



 







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

    



          

    



    



      

  



 

       

















        

     

      

      











      

     









1

e



      

1

 

    e    

       







01



      

   01  

             

               

  







         

          

   









    

   









     

   



    

    















   

           

            

                

            











 





        

   









1

e



         

 





1



e



  



   

1



 

  e



       



0  0 

       



  

          











0



1



  













     0



1



       

      



         



 

   









      







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

        



                 

  







          

  

      

    x

x

   

  









   









       

  x

x

x

x

1  



     

         

x

x

x

1

               





                  

               











  

        





   







         

     x

x

      x

x

 

   







  x

x

  

  x

x

  















  









  x

x

x

   









      

  x

x

   

x

x





x

x







x

x



   



  





















 

















































                  

                 

                

  

           



    

           









    



            

     

        0  1       





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  x

  







  







  

  











 









 







       





 





       







    

            









               





1 1 1



-times

       

01 1 1



-times



   



















  















   

    

a 













 a                

 







    

m

m



 m

    



   





         



















  







 



















               









  



     

             

  







        



    







  







 

    









      











               

   

         

  







     







  

                 

                     





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                

  

       

  







      







 









  







   







   









                 

 

                



                 

         



   

     





 x

x

x

 x

x

x

1

 x

x

x

x

x

x

x

x

x

       

 x

 x

 x



 x

    x

 

       

             

            



     

        x

x

 x

       

     

               

              

         

      x

x

 x

     x

 

  x

               x

x



       x

x

   

                

x

x

  







    







    









 











       

  







   







  







































              x

x

x

     

 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  









      









  













































       







 







  

  







   







  







  













 













  x

x

x

x

  







    

  









                

       

                

 x



x

x

x

x

x

x

x



                   

                 

                  

               

x

x

x

x

x

x

x



           

                  

           

1.2.2 Morphisms, theories, and decidability

               

           

              

       

   







       

        

 



























     











 













 













    









 

 







 





         



   

       



       

    



  



           

 



         







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

       



       



         

 

              

       

    

        

             

 

                 

     

  

              

      

             



    

   

x

x

e x













x

x

x

x

x

x

x

x



x

x

x

1

e

x

x

1

x

e

             

   



  

          

x

x

0x

x

x

1

     

             

                 



 

  

 

  



    



       

 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

               

        

                 

                

     

               

          

             

       

Th



    



     

        

H10







x

x

x

x

   



           

        











x

x











x

x







is atomic for , and 



             

                

      



    

x

x

0x

x

x

1

       Th    







    

      Th

  x

x

1 0         

 



       H10



     

  H10





     











[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

             

x

x

Ex

x

Ex

x

Ex

x



    x

    x

x

       Th





              

                  

         



      

     



          

 



            

               

















           

      



   c





  

                 

 





       













    



  



   

       

H10







x

x

x

x

   



      



     

        













x

x











x









is atomic for , and 



        



     

       













there exists an atomic formula with

, or and 



   



     



     

                 

   

            







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

        



       









 







       





   



P 









     P  

H10     

     



          

 











           

    







    

         



















  

















     



x

x



               

        

  P       P     



  

x

x

x

x



 



      



      

  







 











         





 





    









  













      







          

  



  

x

x

x

x

0

 x

x

         

  H10              

x

x





x

x





x

x



  



 







                 

  











 







































        







   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                  

                   

             

         





x













                

    









              

 x

   

-times











    

s 













 



     



x







































 



   

               

              

      



                 

    





x

x

0

         

        x



   0 1

              

       

s 









   



































    

            



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

H10

∗

(𝔄)

∃+

(𝔄)

Th(𝔄)

𝐷(𝔄)

H10(𝔄)

𝐷

∃+

(𝔄)

𝐷

𝑐

(𝔄)

                  

  

  







  

               

      

                

                   



 Th



  





 H10







x

x

x

x

 



 Th











x

x











x

x







is atomic for 



 











  





 H10







x

x

x

x

 





 











x

x











x

x







is atomic for 



 

 











there exists an atomic formula with

, or 



              

           

   



ThH10



Th







H10







   

    



ThH10



Th







H10









    



         







0 1



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

H10

∗

(𝔒

𝐾

)

∃+

(𝔒

𝐾

)

Th(𝔒

𝐾

)

𝐷(𝔒

𝐾

)

H10(𝔒

𝐾

)

𝐷

∃+

(𝔒

𝐾

)

𝐷

𝑐

(𝔒

𝐾

)

𝒦

       



       













           





  





 

               

                 

                   

        



     

    

          



      

 Th







    H10







  







  

 H10







              

         







    

                

        

1.2.3 Computable structures and decidable models

                

              

               

             

              

                

      

 



       







   

          

             

                









             



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

        

   ar    

                  

            

     

              

        

             

   







            

            

        

                

  

                 

                

     

               

            

             

           

             



                

   FC     R  

F

























        











R









  















        









 

C



             

     

              

   



   

             

   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

           



 

 



      



  

            

   







 



  





        



  



     

       







    















 

















   





             



  

         



       

 

















     













    















       



    

              

             

           

  

                

   

        

        





      

      







     

           



      

  



           

              1 

            

   



            

 

                

 1               

               

11011

   0   1     1

           







 

  







    



        



  

   







  







     











[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

                

            

        



 

           

         







       

            

          









 





















 























 







    





















 





          

             

              

    

              

               

             

  

   



       



 

   







   

  



    



         

                

               

      



        

                

               

          

                

              

            



                  









         















  



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

          

















 



 



 















 



 



     

   









        



 



 

       

            



     

   



          

               

          



 

     



 



        

         0





0





  

c

n1





c





1







 c

        

              

               

     

            



 

   H10 

    



          

     



  

  x

x

x

x

     



 

      







    







  









  









             

 



 









  









      H10    

1.3 Prerequisites from number theory

1.3.1 Number elds and rings of algebraic integers

                 

               

                 

               

          





 



               



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

               

         







     

  







  







     









        







































   











 

            

                  

            

              

              

 



 











          





         

















 

























       

               

                





           

    



          

      



    

                 

              

 

            

                   



















    







          

                

    

                 

                

   

              

     

           



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

              

  

           

             











































              

           



 



    

       



      



 

    





































       







 







     

  















 













        

 

















 

       

            











































   







  







 



























































  

                

     

            

        

  



                



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  



    

                

               

               



   

     



            

     



       

   



          

                

       







       

      



            

             

        



       

      







       

      



       

           



   



 

  







     



     

    



         





 



   





       



      



   

   



 







  







    

 



            

   

                  

 



            

   



      



      





















  







   



         





              

     

            

      



     



 

        



       

      









  

               

   

              



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  



  



     











      











           



    

            











   

     

              

                

 







        

 















 

 



















            





               

  

    



       

    

                

         

             

         





     

 



  





 





         

         





     

               

               

          



     

             

             













 













                 

   



   



  



     

              

       



 



   



   

   



 



 



  

       



         





    



   



     



   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

    





















  







          

      



       



 

            





         



     

     



 



          

 



             



















              

               

                   

         



      

       

        



      



 

     





     



            

           



   

            



  

1.3.2 Ideals of 



              

            



   

             

     



  











 



 



      

              

            











 



 









 







 











  















































     

            



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            









  







           

        



      

                 

                   

     

                

                



            



























































                     





              



 

          



  

  

               

    





            

              



           

             



  



     



        

                

            

        



      

                 

           

        







  

              



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

   

























 















































































































































   











































               

           

   



             



             











 











             

  









prime ideal









  



           

 

          









prime ideal







 







prime ideal









       









prime ideal















        

        







   



    

             



      

 



                   

    



   



        



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

   















              

      











   

     









       





 

















     

















 













     









            

                  

  







 







  







      



















 



 



 



 







    































  

















    







  







       

 

           















 

























   







        



 













      















 













         



 







    

          



































     



         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

  







          

    









  







                

 

















 











       















     



  

    



  







  

                

                

 

  



           

 











  





         



     



 







  

     

           









prime ideal









 



       

             

                  











     



        

       



         

        

               

               







                

1.3.3 Geometry of numbers

               

                



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

𝐷

𝑒

     



    

            

           

 











            











             













   

   



        



    

 













              























  













      









 





















              

         

 



    

 







 



  



























  

















              

                

        



      

          

                   

     

        







 

       



        

             



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

          







      









          







    





























          







 



























 

























             



 





            













 

     











    

      

























              

































      



   





     













































        

             











  



        

  

                

                

         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

   



    



   



     

  











  







     





                









      

























  



  

      





         

     

       

















 















  

















                 

     

































































































































































































             

              

      

   









   







        

       



   

    



       

          







  









 

               





   

    

               



     

              





       



       

           



 



 

    



 



         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

      





             









    



















            









      

























































 

           



















 















   

             









   

          



        

   



               



                 





             

    







 



  

                    

    



              

 



             



             

            

              



  







             













          



   

















       



      









                  

               

        







 





















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

 







      















   

            

   







 



















    



    



   



























       



















     



      



















             

 



        

                

                 

            

       

          

       









   































          



      

               

              

            

          

            

            

                 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

       













 

          



      

           















          

  























































          



       

 







         













      

















           

              

               

              

              

            

                  

              

                 

    



  

             

                 

         

         

              

 



     



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

ႼႵᆡ

ႼႴᆡ ႼႳᆡ

ႼႲᆡ Ⴒᆡ

Ⴓᆡ Ⴔᆡ

Ⴕᆡ

ႼႴᆡ

ႼႳᆡ

ႼႲᆡ

Ⴒᆡ

Ⴓᆡ

Ⴔᆡ

Ⴑ

ᆂ

           

;

0 + ℤ = 1 + ℤ

                      

 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    



          



                

 



             

      

     















 

















                

             



   



























































         























      

             

          



















              



















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

       



    

           

          

      







       

 







  















     













      













        













           















       











 





















              



 

      



         



   

    













    

















  







     



     













 

  

       







             







   

      







     







 















 

              

   

                  

               

               





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

  







  











   







       



 

        











   









            

 



























































    



























  

















          













   



   















   











































































































































































   





























































      



 



        

      











      







 





















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

        









































































   

































       







        













     

    











     





























































 

                 

           

 













  



 



     







  

 











 





 



   



















   



  



 



  























      















      















          

1.3.4 Absolute values and local elds

              

               

                 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

            

        

    

   

    

 

         

       



     



               





    



  



   

            

       



 



   









         



  



    

           



























 





                 





    





  



     







       

  



              

 







             

  



    

     



        



  









    



 



         



          



                 

                  

                 

             



     

        



        



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

    



             

          













                  

             

               

              

               

           

             

    

























   















    

 







          

                 

    







      













































 





  



 



 



   







             







  









     







     

             

            

                 

                  

               

               

          

            







  

       







































   







     







  











       



































    

              

 



          



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    

        







   



  



























                 





           



 







        

 















  





























      

           



 

         





















     

 







            



     









        



   

           



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

2 Hilbert’s tenth problem

2.1 Dierent perspectives on an old problem

2.1.1 Diophantine equations and sets

              

        

    

                

               

   

        

           

              

           



        











 







        









                  

                

        

      

                   

                   

      

     







      



  1 

    0 

              





  



                  

0  1              

     

 

             

               

                   

   

      



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

         

                









   1      0 

                

α  α              

   



            

















           





          















   



              

 



              

          



     

     















  

 









  

























  







       









  









     



       







 









  

























                

 

             

  

   



      

   







          

           

           



   







 

            



  











               

              

   











[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      

𝑥

+ 𝑦

= 1

−1 ≤ 𝑥 ≤ 1

         

     

           







 

  



      



























      











    











 

           







  











       



      











 

 



            

  





                 

 



            

    

        







 









 







 











              

   

























  

























          









 







     





 



 



 







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

    





 





      







       



 



                 

      

  

                

               

           

          

                   

    



            

           

     











        

       





















 

















 

































 





















 



   







  



 



        







 





  



 



     



















   

































































    















    



 



    



















































            

        

  







































               

               

  



        

















 









  



























[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      

                  















































































           

                



















   



 



        



















               

   



 



    































































































































        













































































































































































           







    











               

             



  



          



 x

x

y

y

 









  y

y









y

y





      















        

      



















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

                

                

                

         H10      

     

     H10

               

     

             

  







   









 









               

       



 





            

             

   



   

  

















 

















  

 



 



          







  

       







 





      

 



             













    



 



   



























              

       



















          







  

         

























   



  



    



   

 









































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      

     







 







    



 





    









 

















 







 















































































           







 





 











































































                  

  

            

             

            

              

               

      

  



         

       









           



  

       



 











             

             

               







          



  





    H10

             



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

                

         









    







  







   

               

       







     

        











    

             

            

2.1.2 Purely Diophantine sets

          



     

     















  

 









  

























         

              

               

         

             



  



           



 x

x

y

y



 









  y

y









y

y





               

               

                 

                 

            



   

               

              









               

          

   













           

             

       

                

         



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      

              

                 

           

         

                 

         





  



   

     



 



        





 





  















   





             

   

              

             

 







     







    





            



 

   



           













    



          

             

      











  







 

   

       



   



















      

















      

  









                 

       











     



  







      



 

               

            

         





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

             

     

      

   



              







             

  







     







   

         

  



















        

 









  





























             

  

                 

  



   







 

    



     















 



 

      



     

         



  















           



    



         



   







   

 



 

  

















                

  



  





















        

























[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      

H10

∗

(𝔒

𝐾

)

∃+

(𝔒

𝐾

)

Th(𝔒

𝐾

)

𝐷(𝔒

𝐾

)

H10(𝔒

𝐾

)

𝐷

∃+

(𝔒

𝐾

)

𝐷

𝑐

(𝔒

𝐾

)

𝒦

              



























































           





  





     



         

            















    



     



     



    



  



    



    



















  



              









    

               

        

              H10









        

2.1.3 Related problems

                 

               

              



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

Th     

         

               

           



    

     Th



        

             

            

 

             

     

                 

            

         H10    

   

               

           

  







































  













































              

   



          

      

       



    

             

           













   

  





















       





y

y





y

y

 

   H10         

        H10

     H10    

                   

             



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

                 

               



 

                 

               

                 

                

               

                



                

             



   

              

    

               

 

2.2 Some structural results

              

              

 

   







         



  

  





   



 



     



  

  



  



        



  

     





  







       



 



  







  



     























            

    





















 











      





              

                

   

             

            H10 

   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

             

           

          

                  

           

            













 

  



















 

             

     H10

      



         





                  

  



       



       

    

               

    



           

 H10







 





                   





              

           

     



         

             















               

 H10







        

                

       

 

         



      

   



          

 





   





  



       101 

         



 







-times



  





-times

 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

               





       





 





   













     



   

        





















































                

     



         

            





















































   





















































































































         



     

                 

 





                 

            



   

     



           

            

      



 



      

              

                    

           

            



 

 

























   





















   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

  



 

 







         







           



      

  















      







































    



       

       

            







   

    



     

















 











  

   







   







     





















  





















 































      

















     











[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

       













       







  

   







    





















































  









                   

               

   

    



































        



        

       



         

   













    



  

















 



      





  



































 























        





  











      









  



























     



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

        





































     



































     















        















































 



                

              

   





         



    

      









     





































        









 







  

















































 



      



           

          



   

    



         



     

        

 



         















 























      



      



  







  

     































































                 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

              

  



































































                 

   



         

















      







         

2.3 Hilbert’s tenth problem over totally real number elds and

number elds with one pair of non-real embeddings

                 

                

              

                

                  

             

2.3.1 Finitely many easy lemmas

           









 

               

     



  

 

       



       





  







      

    











 













 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

      



       

          



     

 















      



    

 



 



          

 



               

   



 



       

   

              

   





 





 





     















      

      



       











 

   



             

  











 



          





     









 







      

 













   

















  



          





























































even































odd





















    













even





















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56















odd





















               

     

         



   

     



      













 

 







        



 

    







 

            



 



   

           







      

  







 























  













































     































 

  

























         











 



     



            

        











        



 



  

 

         



    

  



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

 











 











   

 























 























         













  



















 

   



 











  











  



  

      



 



 





































































 

















































   



 



 

       















 











 

             



          



         

   

 



 



 





 

























 



   

    



 



    



  

                 



















              







 







  

 









     



























































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56















odd



























           





   











 

    









 

  







        



















       







        

                

 



 



             

           

         



      

     

















 





















 









         



      

      

















 





























 













  











 













         

        



     

     





 



 

     







  







 

               

  



         



 





                

   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

        













 

 

            



 



  

           

























 

  



 

        



     

       



















             



 





    





















































































          

                 

     





          



         

       



















         

                

  







































































          



         













     



 







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

       



       

 







  

    







  



       

















     



  



 

     











      













     







    







 



    



















     







 



          



 

   



    















  







   



       



    















 





       



  







  







  



    







     









             



  



 

 







 



 















 



       



       



 





           







    

  



          



  



 







        



     











       





          











  



 



  

   



 





         





























        

























   



          

     









































































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

   









   













































































































































           

            

















   





    











 



  



      











     



 







  







  









   



  







       

          

   

  



         













   













     













-times

    











 























      



 



 











      

















              

     













 

                



     

              

               



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

     





  





  

                 

                

                

             

   



       

             

             

           

2.3.2 Diophantine denition of over 

                  

              

     



         



   

               

        



     



    



 

           



    











     



 











       

     



       



 









       







       

      

            































 























 

















 

 

 







    

     



  







   

     



       



    







    

           











   

           



 





[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

                

             



























 



     















      



 















































 



 





      

      



         

     



































      



 



















































































      



























































  



































       



        







         



      

    



  



         









 



     



  

         



   





















          



     



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 



 



        





 





  

























 





























  



  

        



    



  

            



   

  

  



  



 



    

  



     

           



    

       







     

      



       

 



 



             

  



 



     





 



 

 











 



          

  

            



   

   



          

 











  

 



 



    



 

 







 





                  

          





























































  



   



      



  

   



    



      





 



           

       









               

   

           



   

    



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

 









 





























 

 









          







 





         



 

       







  







  

       

              

       

     







      

  





              

         



        

 





 













    









             

  



     







 





  

       

 











 





 



 





  



 



 



 







  

        

 









 





      

      







 

























































































     



   



























        



  



  



      

























































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      





















   

               

      



    

               

      

     



             

























   







 







   































































  



 







   











 

















































  











   







          















    

   













































    



















































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

               















by (iv)

 

        















         







 

     







      

        

        

     

     



           

              









                  



             





    



        





      





             

            



     



          



 

    





          



    

     

         



    





          











     









 



























          









 



























  



  



  





   















[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

  











       





  



     

  





























  















        





































 

  





             













































         





















































































 

      















































































































































         



    

           





               











 



    





















    

       











     











 























[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

      



















  

















   

 





























































 



       







       

    



    











     

   



      



      



   







 







         

             





  











           



    



 





                   

                 

                

     

               





      







     





















 

    



      











       

             

        



  













   











































   















      

     



       

        











































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

          









even





































odd



























           







 









         



    

 











      





       



  







   













































 



   







     







  



    

  

         



     

       







   

 



























 





            



 



 

     











 













 

















      

















   

          



     



 











 



          



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

 

















              

 



   







 



 



























  















        

     



























  















    



 





























                 

   













































































































            

     

 



 







  



 



 



        

  















 



























   



  



























      



 











      





































       



















     



 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

























































































         

      



 















  



   





  











      



    

         



   

















   





             





   



  



 



           









 







    















   







































   



      









































  



 











  



     























































































  















     



  



























      

























































































































































































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

  



      

















  







 







        



  































   

               



 

 



          







  

    









































        

 







 



  

 









 



 



 





         



         

             



 



 

   





































































































































































              



 





  























        







  









































































































































































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

      





        

















 

 







         

  









Lem. 2.3.3.(ii)

 

















      







  











 



     

      



 



    



   

 







    







  

   

        









 



       

                 







































even































odd

























  



 



      



























   



  



  





          





            



  





















 



       







   













 



   

  







  







 







    

    







   

























  

























        











 



     













   







    







 











   

  

























 

           







   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

  









 





                 

 









































































































































             





   

    











          













































































































    











































































































































































      



  



















   

























   



         

























































































 

       



   







































         



























             



  



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

  



  





 





















     





  

















































































































































































       







     



  

   



 









         























    

       







 











     

       











 







      

     











 























   

    















































































 







         















































































 









            



   

  







   







      

  





  



 

  







  



 







  



 

             

 





























































[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

              



 





    























   











 



       

         







 





            























































  



              

















 















          

  







 







      









              

    







   



  













































        









      



















































































 



  



 



  



    

    



 































































   



          



  









     



       













































  













































      



         









 







  



  

             











            



 



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 







          



    

   



         



  







              





 

  











































































































































































  



 





 









  



 

 





 

    

  

  



















 

             

              



   

      

                

      

             

                 

                





 



       



 





          



       



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

   





















































 























  



           





           

 

               

 





 









 









 









 





         









 













  



 





 











 

 



  



 









 



 





 



 

       





 

    





 





          

 



 

            









 







[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

    









 





         



      

  

            





  



           

 





        

 





        

























           

































               

          



 

              

















 







         



 



           



 



























      



 



      

  



 







  



       



  

      



 



     











   









     



 



   



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

              



  







 





             



  









  



     







 



 

   



 



 







       

  



       









 







           

        

                 

            





           



       

           































































               



               

              

                

               

              



               

               

                

         

               

 



         

           

             

  H10



           

             H10



  

                

               



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

A Collected Haskell implementations

A.1 Simulating Turing machines

            https://github.com/

tim6her/h10-turing-machines              

 

git clone https://github.com/tim6her/h10-turing-machines.git

cd h10-turing-machines

cabal setup && cabal build && cabal install

              ghci  

              

             

>>> import Automaton.TuringMachine

>>> :l tally

>>> let d = toTransition tally "error" -- mark the errornous state

>>> let turing = TuringMachine "start" '_' "halt" d

>>> "§1111" >>> turing -- Tally encoding of 4

Just "§1"

>>> "§1011" >>> turing -- Not tally encoded

Just "§0"

             

A.2 Polynomials

             

             

        

          

{-# LANGUAGE RebindableSyntax #-}

module Monomial

( Monomial

, (<*>)

, idt

, mfromList

, clean

) where



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

import NumericPrelude

import Data.Map (Map, delete, empty, foldrWithKey, fromList, member, insert,

insertWith, (!))

import Algebra.Monoid as Monoid

import Test.Tasty

import Test.Tasty.HUnit

import Test.Tasty.QuickCheck as QC

-- | Monomials are mappings from ZZ to NN with finite support

newtype Monomial = Monomial (Map Integer Integer) deriving (Eq, Ord)

instance Monoid.C Monomial where

idt = Monomial empty

(<*>) = mmul

instance Show Monomial where

show (Monomial m)

| m == empty = "1"

| otherwise = foldrWithKey

(\x e sh -> "X" ++ show x ++ "^" ++ show e ++ " " ++ sh)

"" m

-- | Creates monomials from list of tuples

-- Left entry is index of indeterminate, right index is power of the

-- indeterminate

-- === Example

-- >>> mfromList [(1, 2), (0, 3), (4, 7)]

-- X0^3 X1^2 X4^7

mfromList :: [(Integer, Integer)] -> Monomial

mfromList l = clean $ Monomial $ fromList l

-- | Multiplies two monomials

-- === Example

-- >>> mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])

-- X1^2 X2^5 X3^2

mmul :: Monomial -> Monomial -> Monomial

mmul xx@(Monomial m1) yy@(Monomial m2)

| m1 == empty = yy

| m2 == empty = xx

| otherwise = clean $ Monomial $ foldrWithKey



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 

(\x e m -> if x `member` m

then insertWith (+) x e m

else insert x e m)

m2 m1

clean :: Monomial -> Monomial

clean (Monomial m)

| m == empty = (Monomial m)

| otherwise = Monomial $ foldrWithKey

(\x e m -> if e <= 0

then delete x m

else m)

m m

-- * Testing

main :: IO ()

main = defaultMain tests

tests :: TestTree

tests = testGroup "Tests" [properties, unitTests]

properties :: TestTree

properties = testGroup "Properties" [qcProps]

qcProps = testGroup "Axioms of monoids"

[ QC.testProperty "left multiplication by identity" $

\x -> (let m = mfromList (x :: [(Integer, Integer)])

in idt <*> m == m)

, QC.testProperty "right multiplication by identity" $

\x -> (let m = mfromList (x :: [(Integer, Integer)])

in m <*> idt == m)

, QC.testProperty "associativity" $

\x y z -> (let m1 = mfromList (x :: [(Integer, Integer)])

m2 = mfromList (y :: [(Integer, Integer)])

m3 = mfromList (z :: [(Integer, Integer)])

in (m1 <*> m2) <*> m3 == m1 <*> (m2 <*> m3))

, QC.testProperty "commutativity" $

\x y -> (let m1 = mfromList (x :: [(Integer, Integer)])

m2 = mfromList (y :: [(Integer, Integer)])

in m1 <*> m2 == m2 <*> m1)

]

unitTests = testGroup "Unit tests"

[ testCase "show X0^3 X1^2 X4^7" $

show (mfromList [(1, 2), (0, 3), (4, 7)]) @?= "X0^3 X1^2 X4^7 "



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

, testCase "sample multiplication" $

show (mmul (mfromList [(1, 2), (2, 4)]) (mfromList [(2, 1), (3, 2)])) @?=

"X1^2 X2^5 X3^2 "

, testCase "test clean" $

mfromList [(1, 0), (2, 0), (3, 1)] @?= mfromList [(3, 1)]

]

          

{-# LANGUAGE RebindableSyntax #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE MultiParamTypeClasses #-}

import NumericPrelude

import qualified Monomial

import qualified Data.Map as Map

import Algebra.Monoid as Monoid

import Algebra.Ring as Ring

import Algebra.Module as Module

import Algebra.Additive as Additive

import Test.Tasty

import Test.Tasty.HUnit

import Test.Tasty.QuickCheck as QC

-- | Polynomials over a ring R are finitely supported functions

-- from the set of monomials to R

newtype Polynomial a = Polynomial (Map.Map Monomial.Monomial a)

-- | Polynomials form an additive (abelian) group

instance (Ring.C a, Eq a) => Additive.C (Polynomial a) where

zero = Polynomial Map.empty

(+) = padd

negate (Polynomial m) = Polynomial $ Map.map negate m

-- | Polynomials from an R-module

instance (Ring.C a, Eq a) => Module.C a (Polynomial a) where

(*>) 0 _ = zero

(*>) a (Polynomial m) = Polynomial $ Map.map (a*) m

-- | Polynomials form a ring with unit

instance (Ring.C a, Eq a) => Ring.C (Polynomial a) where

one = pfromList [(1, [])]

(*) p@(Polynomial m1) q

| p == zero = zero

| q == zero = zero



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 

| p == one = q

| q == one = p

| otherwise = Map.foldrWithKey

(\mono coeff poly -> (coeff *> mono `mmul` q) + poly)

0 m1

-- | Two polynomials are equal if their difference is zero

instance (Ring.C a, Eq a) => Eq (Polynomial a) where

(==) p q = let (Polynomial m) = p - q in m == Map.empty

instance (Show a, Eq a) => Show (Polynomial a) where

show (Polynomial p)

| p == Map.empty = "0"

| otherwise = Map.foldrWithKey

(\m a sh -> show a ++ " " ++ show m ++ "+ " ++ sh)

"" p

-- | Adds two polynomials over the same ring

-- If a coefficient of a monoid equals 0 the monoid is dropped out of the map

padd :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a -> Polynomial a

padd p@(Polynomial m1) q@(Polynomial m2)

| m1 == Map.empty = q

| m2 == Map.empty = p

| otherwise = clean $ Polynomial $ Map.foldrWithKey

(\mono coeff poly -> if mono `Map.member` poly

then Map.insertWith (+) mono coeff poly

else Map.insert mono coeff poly)

m2 m1

mmul :: (Ring.C a, Eq a) => Monomial.Monomial -> Polynomial a -> Polynomial a

mmul mono poly@(Polynomial mp)

| mono == Monomial.idt = Polynomial mp

| poly == zero = zero

| otherwise = Polynomial $ Map.mapKeys (mono Monomial.<*>) mp

-- | Generate polynomials from lists

pfromList :: (Ring.C a, Eq a) => [(a, [(Integer, Integer)])] -> Polynomial a

pfromList [] = zero

pfromList ((a, m):l) = deepClean . clean $ (Polynomial $ Map.singleton

(Monomial.mfromList m) a) + pfromList l

-- | Comfort function for creating polynomials

-- === Example



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

-- >>> 2 *> ((x 1 + x 2) * (x 1 - x 2)) == 2 *> x 1 ^ 2 - 2 *> x 2 ^ 2

-- True

x :: (Ring.C a, Eq a) => Integer -> Polynomial a

x i = pfromList [(1, [(i, 1)])]

-- | Remove monoids with coefficient zero from support

clean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a

clean (Polynomial m) = Polynomial $ Map.foldrWithKey

(\mono coeff poly -> if coeff == 0

then Map.delete mono poly

else poly)

m m

-- | Remove variables with power zero from monomials

-- This function runs in O(n log(n)) so use it sparsely

deepClean :: (Ring.C a, Eq a) => Polynomial a -> Polynomial a

deepClean (Polynomial m) = Polynomial $ Map.mapKeys Monomial.clean m

-- * Testing

main :: IO ()

main = defaultMain tests

tests :: TestTree

tests = testGroup "Tests" [properties, unitTests]

properties :: TestTree

properties = testGroup "Properties" [qcAddProps, qcModProps,

localOption (QuickCheckTests 5) qcRingProps,

qcAlgebraProps]

qcAddProps = testGroup "Group axioms for addition"

[ QC.testProperty "addition is commutative" $

\x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

q = pfromList (y :: [(Int, [(Integer, Integer)])])

in p + q == q + p)

, QC.testProperty "addition is associative" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in (p1 + p2) + p3 == p1 + (p2 + p3))

, QC.testProperty "addition by zero" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in p + zero == p)

, QC.testProperty "addition with inverse" $



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in p - p == zero)

]

qcModProps = testGroup "Module axioms"

[ QC.testProperty "first distributive law" $

\a x y -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

q = pfromList (y :: [(Int, [(Integer, Integer)])])

in (a :: Int) *> (p + q) == a *> q + a *> p)

, QC.testProperty "second distributive law" $

\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (a + b :: Int) *> p == a *> p + b *> p)

, QC.testProperty "multiplications commute" $

\a b x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (a * b :: Int) *> p == a *> (b *> p))

, QC.testProperty "multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in (one :: Int) *> p == p)

]

qcRingProps = testGroup "Ring axioms"

[ QC.testProperty "multiplication is associative" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in (p1 * p2) * p3 == p1 * (p2 * p3))

, QC.testProperty "left multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in one * p == p)

, QC.testProperty "right multiplication by one" $

\x -> (let p = pfromList (x :: [(Int, [(Integer, Integer)])])

in p * one == p)

, QC.testProperty "distributive law" $

\x y z -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

p3 = pfromList (z :: [(Int, [(Integer, Integer)])])

in p1 * (p2 + p3) == p1 * p2 + p1 * p3)

]

qcAlgebraProps = testGroup "Algebra axioms"

[ QC.testProperty "multiplications commute" $

\x y a -> (let p1 = pfromList (x :: [(Int, [(Integer, Integer)])])

p2 = pfromList (y :: [(Int, [(Integer, Integer)])])

in (a :: Int) *> (p1 * p2) == (a *> p1) * p2)

]



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

   

unitTests = testGroup "Unit tests"

[ testCase "sample polynomial" $

show (pfromList [(1, [(1, 2), (3, 4)]), (-4, [(1, 4), (2, 3)])]

:: Polynomial Int) @?= "1 X1^2 X3^4 + -4 X1^4 X2^3 + "

, testCase "test equality" $

pfromList [(0, [(1, 1)])] @?= (zero :: Polynomial Int)

]



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

B Summaries

B.1 Zusammenfassung

            

          

                

            

            

              

            

            

             

           

     

            

          

           

             

          

             

          

            

           

         

        



      

         



 

     

              

             

           

    



        

  



           

              

     



    



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

 

B.2 Summary

               

             

                 

              

                 

                

               

                

                



             

                

              

              

           

               

              

              

               

         



    



  

            





              

                 

               

 



          



   

                

              





        



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

List of Figures

                           

                                      

     

add1

 1101                         

              

                                      

                

                                

             

                       

      



     

  











                              

    



                     

                        

                 

                            

                       

           

 



                                     



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56

Bibliography

           

         

   

             

       http://www.jstor.org/stable/2269326

            

        10.2307/2371045

            

   

           

          10.2307/2318447

 http://www.jstor.org/stable/2318447

             

        10.1016/j.amc.2005.09.066 

https://doi.org/10.1016/j.amc.2005.09.066

           

         

          

             

 

              

       10.2307/1998133

              

       10.2307/2040720

             

            

10.1112/jlms/s2-18.3.385

               

        

10.1515/crll.1988.388.189  https://doi.org/10.1515/crll.1988.388.189

             

      10.1112/jlms/s1-8.1.18



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56



              

          

   

            

            

          

            

  10.1007/BF01700692  https://doi.org/10.1007/BF01700692

             

     

            

            

 10.1090/S0273-0979-00-00881-8

         

         

       

          

           

       

10.1007/978-3-642-75306-0

          

            

            

            

     10.1215/S0012-7094-36-00227-2 

https://doi.org/10.1215/S0012-7094-36-00227-2

           

          

         

  10.1007/978-3-642-54936-6_5

            

       10.1007/978-1-4613-0041-0 

https://doi.org/10.1007/978-1-4613-0041-0

             

    

              

            

https://www.ebook.de/de/product/3665990/david_marker_model_theory_an_

introduction.html



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56



           

        

          

www.jmilne.org/math/

           

    http://www.logic.univie.ac.at/~muellem3/TCS.pdf  



        

    

              

         

http://ubdata.univie.ac.at/AC05622932

              

           

10.4310/MRL.2013.v20.n5.a12

               

          10.2307/2047021 

https://doi.org/10.2307/2047021

           

         

http://www.ams.org/notices/200803/tx080300344p.pdf

             

           

             

10.1007/3-540-45455-1_4

             

           

10.1090/S0002-9904-1944-08111-1 

https://doi.org/10.1090/S0002-9904-1944-08111-1

            

          10.2307/2266510

             

         10.2307/2033628 

https://doi.org/10.2307/2033628

            

        10.2307/2266685

             

       10.2307/2269028



[git] • Branch: master @ 1f9ef90 • Head tags: v0.6-1-g1f9ef90 • Compile time: 2019-09-08 17:56



               

        10.1515/crll.1986.368.127





https://doi.org/10.1515/crll.1986.368.127

         

             

  10.1002/cpa.3160420805 

https://doi.org/10.1002/cpa.3160420805

           

            

10.1002/cpa.3160420703

            

           

          

https://doi.org/10.1090/conm/270/04370

           

           

     

http://www.ebook.de/de/product/6433593/alexandra_shlapentokh_hilbert_s_

tenth_problem_diophantine_classes_and_extensions_to_global_fields.html

         

http://math.cornell.edu/~shore/papers/pdf/proc4t.pdf   

             

             

          

10.1016/S0049-237X(99)80028-7 

http://www.sciencedirect.com/science/article/pii/S0049237X99800287

            

      http://eudml.org/doc/212515

           

           

  10.1112/plms/s2-42.1.230 

https://doi.org/10.1112/plms/s2-42.1.230

